tg:Id, l:IdLnk, L:MsgA List.
(A,BL.A ||+ B)
 ((L).din(l,tg)
 (~
 (reduce(M,x. if rcv(l,tg)  dom(1of(2of(M))) M.din(l,tg) else x fi;Top;L)) 

latex

Definitions	Unit, , b, b, M1  M2, if b t else f fi, x  dom(f), KindDeq, rcv(l,tg), a:A fp B(a), Knd, Top, 1of(t), 2of(t), Valtype(da;k), x. t(x), P  Q, x,y. t(x;y), (x,yL.P(x;y)), , M.din(l,tg), mk-ma, Prop, A ||+ B, l[i], {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, Id, IdLnk, x:A. B(x), t  T, MsgA, (L)
Lemmas	msga wf, IdLnk wf, Id wf, select wf, ma-compat wf, int seg wf, length wf2, pairwise-cons, pairwise wf, Knd wf, fpf-trivial-subtype-top, ma-join-list wf, rcv wf, Kind-deq wf, fpf-join-cap-sq, assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert